Nuprl Lemma : w-loc-rcv
0,22
postcript
pdf
w
:World,
e
:E. rcv?(
e
)
(loc(
e
) ~ destination(link(
e
)))
latex
Definitions
False
,
t
T
,
P
Q
,
True
,
b
,
tag(
k
)
,
lnk(
k
)
,
act(
k
)
,
islocal(
k
)
,
kindcase(
k
;
a
.
f
(
a
);
l
,
t
.
g
(
l
;
t
) )
,
x
:
A
B
(
x
)
,
left
+
right
,
Knd
,
x
:
A
.
B
(
x
)
,
x
:
A
B
(
x
)
,
s
=
t
,
ecase1(
e
;
info
;
i
.
f
(
i
);
l
,
e'
.
g
(
l
;
e'
))
,
link(
e
)
,
w-info(
w
;
e
)
,
loc(
e
)
,
rcv?(
e
)
,
E
,
s
~
t
,
World
,
kind(
e
)
Lemmas
world
wf
,
w-E
wf
,
w-ekind
wf
,
Knd
wf
,
true
wf
,
false
wf
origin
w:World, e:E. rcv?(e) 
(loc(e) ~ destination(link(e))) w:World, e:E. rcv?(e) (loc(e) ~ destination(link(e))) 
T Q
b
B(x)x:A. B(x)
B(x)